This section expands the explanation of verification options in Section 2.2.4.
According to each type of assertions supported in CSP module, the possible
admissible behaviors and the verification engines provided in PAT are listed in
the following.
Note: The numbers attached to each option
represents the corresponding options under batch mode
verification and command line
console.
Note: The verification engine
for symbolic model checking using BDD is only available if the system can
be encoded using BDD.
Deadlock-Freeness and
Nonterminating:
- Admissible behaviors: All (0)
- Verification engines:
- First witness trace using Depth First Search (0)
- Shortest witness trace using Breadth First Search (1)
- Symbolic Model Checking using BDD with Forward Search Strategy (2)
- Symbolic Model Checking using BDD with Backward Search Strategy (3)
- Symbolic Model Checking using BDD with Forward-Backward Search Strategy
(4)
Divergence-Freeness
and Deterministic:
- Admissible behaviors: All (0)
- Verification engines:
- First witness trace using Depth First Search (0)
- Shortest witness trace using Breadth First Search
(1)
Reachability:
- Admissible behaviors: All (0)
- Verification engines:
- First witness trace using Depth First Search (0)
- Shortest witness trace using Breadth First Search (1)
- Symbolic Model Checking using BDD with Forward Search Strategy (2)
- Symbolic Model Checking using BDD with Backward Search Strategy (3)
- Symbolic Model Checking using BDD with Forward-Backward Search Strategy
(4)
Refinement:
- Admissible behaviors: All (0)
- Verification engines:
- On-the-fly trace refinement checking using Depth First Search (0)
- On-the-fly trace refinement checking using Breadth First Search
(1)
Failure-Refinement:
- Admissible behaviors: All (0)
- Verification engines:
- On-the-fly failure refinement checking using Depth First Search (0)
- On-the-fly failure refinement checking using Breadth First Search
(1)
Failure/Divergence
Refinement:
- Admissible behaviors: All (0)
- Verification engines:
- On-the-fly failures/divergence refinement checking using Depth First
Search (0)
- On-the-fly failures/divergence refinement checking using Breadth First
Search (1)
Safety-LTL Properties:
Liveness Properties: (for the
meaning of admissible behaviors with fairness assumption, please refer to Section 4.1)
- Admissible behaviors:
- All (0)
- Event-level weak fair only (1)
- Event-level strong fair only (2)
- Process-level weak fair only (3)
- Process-level strong fair only (4)
- Global fair only (5)
- Verification engines (same for each admissible behavior above):
- Strongly connected components based search (0)
- Symbolic model checking using BDD (1)
Process
Analysis Toolkit (PAT) 3.5
Help